Negated types #29317

weswigham · 2019-01-09T01:46:24Z

Long have we spoken of them in hushed tones and referenced them in related issues, here they are:

Negated Types

Negated types, as the name may imply, are the negation of another type. Conceptually, this means that if string covers all values which are strings at runtime, a "not string" covers all values which are... not. We had hoped that conditional types would by and large subsume any use negated types would have... and they mostly do, except in many cases we need to apply the constraint implied by the conditional's check to it's result. In the true branch, we can just intersect the extends clause type, however in the false branch we've thus far been discarding the information. This means unions may not be filtered as they should (especially when conditionals nest) and information can be lost. So that ended up being the primary driver for this primitive - it's taking what a conditional type false branch implies, and allowing it to stand alone as a type.

Syntax

not T

where T is another type. I'm open to bikeshedding this, or even shipping without syntax available, but among alternatives (!, ~) not reads pretty well.

Identities

These are little tricks we do on negated type construction to help speed things along (and give negations on algebraic types canonical forms).

not not T is T
not (A | B | C | ...) is not A & not B & not C & not ...
not (A & B & C & ...) is not A | not B | not C | not ...
not unknown is never
not never is unknown
not any is any (since any is the NaN of types and behaves as both the bottom and top)

Assignability Rules

Negated types, for perhaps obvious reasons, cannot be related structurally - the only sane way to relate them is in a higher-order fashion. Thus, the rules governing these relations are very important.

A negated type not S is related to a negated type not T if T is related to S.
This follows from the set membership inversion that a negation implies - if normally a type S and a type T would be related if S is a subset of T, when we take the complements of those sets, not S and not T, those sets share an inverse relationship to the originals.
A type S is related to a negated type not T if the intersection of S and T is empty
We want to check if for all values in S, none of those values are also in T (since if they are, S is not in the negation of T). The intersection of S and T, when simplified and evaluated, is exactly the description of the common domain of the two. If this domain is empty (never), then we can conclude that there is no overlap between the two and that S must lie within not T.
A negated type not S is not related to a type T.
A negated type describes a set of values that reaches from unknown to its bound, while a normal type describes values from its bound to never - it's impossible for a negated type to satisfy a normal type

Assignability Addendum for Fresh Object Types

Frequently we want to consider a fresh object type as a singleton type (indeed, some examples in the refs assume this) - it corresponds to one runtime value, not the bounds on a value (meaning, as a type, both its upper and lower bounds are itself). Using this, we can add one more rule that allows fresh literal types to easily satisfy negated object types.

A fresh object type S is related to a negated type not T if S is not related to T.
Since S is a singleton type, we can assume that so long as it's type is not in T, then it is in not T.

Examples

Examples of negated type usage can be found in the tests of this PR (there's a few hundred lines of them, and probably some more to come for good measure), but here's some of the common ones, pulled from the referenced issues:

declare function ignore<T extends not (object & Promise<any>)>(value: T): void;
declare function readFileAsync(): Promise<string>;
declare function readFileSync(): string;
ignore(readFileSync());     // OK
ignore(readFileAsync());    // Should error

declare function map<T, U extends not void>(values: T[], map: (value: T) => U) : U[]; // validate map callback doesn't return void

function foo() {}

map([1, 2, 3], n => n + 1); // OK
map([1, 2, 3], foo);        // Should error

function asValid<T extends not null>(value: T, isValid: (value: T) => boolean) : T | null {
    return isValid(value) ? value : null;
}

declare const x: number;
declare const y: number | null;
asValid(x, n => n >= 0);    // OK
asValid(y, n => n >= 0);    // Should error

function tryAt<T extends not undefined>(values: T[], index: number): T | undefined {
    return values[index];
}

declare const a: number[];
declare const b: (number | undefined)[];
tryAt(a, 0);    // OK
tryAt(b, 0);    // Should error

Fixes #26240.
Allows #27711 to be cleanly fixed with a lib change (example in the tests).

Ref #4183, #4196, #7648, #12215, #18280

DanielRosenwasser · 2019-01-09T21:03:33Z

tests/baselines/reference/keyofAndIndexedAccessErrors.errors.txt

@@ -46,7 +46,6 @@ tests/cases/conformance/types/keyof/keyofAndIndexedAccessErrors.ts(87,5): error
 tests/cases/conformance/types/keyof/keyofAndIndexedAccessErrors.ts(103,9): error TS2322: Type 'Extract<keyof T, string>' is not assignable to type 'K'.
  Type 'string & keyof T' is not assignable to type 'K'.
    Type 'string' is not assignable to type 'K'.
-      Type 'string' is not assignable to type 'K'.


I'm not complaining, but why'd this go away?

I accidentally fixed a bug where we duplicated the elaboration - this is as the same as the line above.

DanielRosenwasser · 2019-01-09T21:19:20Z

First take, without having tried this out:

Intersections appear to be the correct mechanism to check for potential overlap, but that also means almost no object type can satisfy a negated object type. If we add negated types, I would prefer not to give the check up at all though.
I find it weird, but understandable, that you treat fresh object types differently. But it's clearly weird that these are the only exception to the above issue.

I do have some reservations on the feature for these reasons. If you think about our features trying to satisfy convenience, intent, and safety, then I don't know if this appropriately weighs convenience and intent.

weswigham · 2019-01-09T21:42:06Z

Intersections appear to be the correct mechanism to check for potential overlap, but that also means almost no object type can satisfy a negated object type. If we add negated types, I would prefer not to give the check up at all though.

not (object & SomeInterface)

It works just dandy~

DanielRosenwasser · 2019-01-09T21:54:43Z

It works just dandy~

What do you mean? Yesterday you mentioned that you couldn't assign an array to a not PromiseLike<any>.

weswigham · 2019-01-09T21:59:11Z

Nope, you can't, because you can trivially make a

interface PromiseLikeArray extends Array<any> implements PromiseLike<any> { /*...*/ }

so, if you go to the example, I just state that I explicitly return an array that isn't PromiseLike - that is T[] & not PromiseLike<any>

weswigham · 2019-01-09T22:21:59Z

Per offline feedback from @ahejlsberg I've changed from ~ unary operator to a not keyword type operator (and updated all the text in this PR thus far to match). It does read nicer.

Jessidhia · 2019-01-10T05:17:40Z

Can this be used as a way to restrict the potential type of unbounded types? For example, number & not 0 to allow any number except the literal 0.

This doesn't look very useful at first glance but it can be powerful on mapped types. For example, [key in string and not keyof CSS.Properties<any>] in https://github.com/DefinitelyTyped/DefinitelyTyped/blob/e836acc75a78cf0655b5dfdbe81d69fdd4d8a252/types/styled-components/index.d.ts#L16-L25 could allow the constrained index signature to not have to include CSS.Properties<string | number>[keyof CSS.Properties<string | number>].

weswigham · 2019-01-10T06:41:03Z

Can this be used as a way to restrict the potential type of unbounded types? For example, number & not 0 to allow any number except the literal 0.

Yep. That's a primary driver for 'em.

Jessidhia · 2019-01-10T10:11:53Z

type Exact<T extends object> = T & Partial<Record<not keyof T, never>>

🤔

jack-williams · 2019-01-10T11:01:45Z

Is there an outline of how not interacts with narrowing? Might we have something like?

function foo(x: unknown) {
  if (typeof x === "number") {
    const num: number = x;
  } else {
    const numNot: not number = x;
  }
}

Assignability Addendum for Fresh Object Types

Is there a short example that demonstrates wanting a not for an object literal?

@DanielRosenwasser Do you mean something like { x: number } is not assignable to not { x: boolean } because { x : number} & { x: boolean } does not get reduced to never.

Meta question for @DanielRosenwasser: You say:

convenience, intent, and safety

that seem like some internal principles the TS team have for designing features? Is there a public description of these? I think it would help feature proposals if external contributors could frame their suggestions with the same language used internally.

@Kovensky I'm not sure that will type-check. The type not keyof T includes any type which isn't one of the keys, such as boolean. You might need:

type Exact<T extends object> = T & Partial<Record<(not keyof T) & string, never>>

though I'm not sure what the semantics will be for not types appearing in mapped type constraints.

weswigham · 2019-01-10T18:07:49Z

Is there an outline of how not interacts with narrowing? Might we have something like?

In this PR no negated types are produced by control flow yet; however we've talked over it and negated types make the lib type facts PR elegant to implement, since we can skip using conditionals (which don't compose well) and just filter with intersections of negated types :D

Is there a short example that demonstrates wanting a not for an object literal?

Aye, a test case with an example I pulled from a related issue:

// from https://github.com/Microsoft/TypeScript/issues/4183
type Distinct<A, B> = (A | B) & not (A & B);
declare var o1: {x};
declare var o2: {y};

 declare function f1(x: Distinct<typeof o1, typeof o2>): void;

 f1({x: 0});         // OK
f1({y: 0});         // OK
f1({x: 0, y: 0});   // Should error

though I'm not sure what the semantics will be for not types appearing in mapped type constraints.

Right now they're quietly dropped (aside from filtering out mismatching concrete types), like symbol for the same reason. There's no non-generic concept to map them into. I have a test to that effect. The arbitrary index signatures PR fixes this and would allow an index signature of a, say, string & not "". With that in place mapped types work correctly with 'em, since the intersections trivially desugar to an index signature.

jack-williams · 2019-01-10T18:38:45Z

@weswigham Thanks! And this PR is very cool :)

Re: the object literal example. Should that not be a case where EPC raises an error? I know it doesn't right now because there is no discriminant, but it probably should. Will using negation types become the canonical way of dealing with examples like this? If not, and assuming EPC does get fixed, are there many other use-cases for the special object literal relation.

weswigham · 2019-01-10T21:18:06Z

Re: the object literal example. Should that not be a case where EPC raises an error? I know it doesn't right now because there is no discriminant, but it probably should. Will using negation types become the canonical way of dealing with examples like this? If not, and assuming EPC does get fixed, are there many other use-cases for the special object literal relation.

Even if excess property checking makes defining a type like Distinct unneeded, you'd still need the relationship to allow a type like Distinct to be satisfiable (with fresh object types) should one be used.

SalathielGenese · 2019-01-15T01:24:57Z

Good job so far, I delayed some projects to wait for this feature - for more than a year.

jack-williams · 2019-01-16T09:56:54Z

Do these identities hold?
T & (not T) is never.
T & (not U) is T when T and U are disjoint.
"2b" | (not "2b") is unknown, or generally T | (not T) is unknown.

Just wondering what it would take to fix #28131

weswigham · 2019-01-16T17:51:42Z

T & (not T) is never.

Yes. More generally, when U extends T, U & not T is never.

T & (not U) is T when T and U are disjoint.

Yes.

"2b" | (not "2b") is unknown, or generally T | (not T) is unknown

More generally when U extends T, T | not U is just unknown (quite literally the opposite of the intersection into never rule). That's correct though I don't remember if I'd actually implemented this one yet - afaik we don't currently have any union identities that cause unions to "simplify" to unknown yet so I remember thinking about how it's best accomplished for a bit.

DanielRosenwasser · 2019-01-23T04:31:41Z

src/compiler/checker.ts

+                        const result = isRelatedTo(source, (target as NegatedType).type);
+                        return result === Ternary.Maybe ? Ternary.Maybe : result ? Ternary.False : Ternary.True;
+                    }
+                    // Relationship check is S ⊂ T


Do you really need to use this symbol? It almost sounds like a joke, but this could affect memory footprint when bootstrapping the compiler since modern engines can avoid full UTF16 representations https://blog.mozilla.org/javascript/2014/07/21/slimmer-and-faster-javascript-strings-in-firefox/

A minification step will simply remove this line. The article suggests to minify the code to utilise the inline strings and also help with strings interning. I guess, v8 should not be so much different in this sense and also win from code minification.

jack-williams · 2019-01-24T22:30:50Z

@weswigham Seems to work, right?

type UnionToInterWorker<T> = not (T extends T ? not T : never);
type UnionToInter<T> = [T] extends [never] ? never : UnionToInterWorker<T>;

Not quite sure what should happen here:

type NotInfer<T> = T extends not (infer U) ? U : never;
type NotString = NotInfer<string> // string extends not U ? U : never;

Currently it doesn't reduce; maybe infer types should be disallowed under not?

weswigham · 2019-01-24T22:43:47Z

It doesn't reduce because we don't reduce reducible conditionals with infer's in them right now. IMO, it certainly still makes sense to allow an infer inside a not, since not A extends not infer B ofc should infer A for B.

jack-williams · 2019-01-24T22:54:41Z

Yep, you're right. I guess it could infer U = not string?

qwelias · 2022-05-15T21:50:54Z

Love coming back to this PR about once or twice a year because of not being able to do something.
Is there a chance to get any update on the state of it?

kevinbarabash · 2022-05-24T01:49:46Z

Would support for negated types make type inference involving conditional types easier and/or more powerful?

sandersn · 2022-05-24T22:24:20Z

This experiment is pretty old, so I'm going to close it to reduce the number of open PRs.

jsejcksn · 2022-05-24T23:43:43Z

@sandersn Is that a "no" to negated types, or will the concept be tracked somewhere else now? If the latter, I'd like to know where so that I can subscribe to the new conversation.

sandersn · 2022-05-25T16:24:47Z

Not "no", but discussion should happen on an issue, #4196 probably, instead of a PR. PRs go stale.

weswigham · 2022-05-25T16:56:44Z

(Though admittedly the proposal in the PR description is admittedly way more concrete and detailed than anything in that issue rn, and the blockers for this are less about the syntax and behavior and more about implementation and performance + language complexity concerns, all of which are more tied to this PR specifically than the original idea)

dimitropoulos · 2022-06-01T13:14:41Z

while I certainly can relate to wanting to keep the PR count down to a manageable number (we have the same problem over on insomnia), I would like to echo the above from @weswigham. I've been following this conversation very closely for years, since it and #29729 are the two features I am the most interested in.

I guess at the end of the day as long as this PR isn't locked we can all keep talking here, but it'd be fantastic to have a better understanding of what needs to happen next for negated types to rise-the-ranks a little in the prioritization. I don't want to spam iteration plans (e.g. #49074) with my wants-and-needs... but I'm not sure what else to do at this point.

I hit the need for negated types on a weekly basis. Should I just drop those use-cases in here whenever I hit them?

sandersn · 2022-06-01T22:29:28Z

@dimitropoulos #49220 addresses the scenario in #29729 in a different way.

falfiya · 2022-06-07T01:40:37Z

Thanks for mentioning #49220. I didn't even know I had this problem till I read it. What I'm hearing is that I should follow future discussion of negated types in #4196? They'd be absolutely wonderful to have for stuff like "number without NaN".

Autumn-one · 2023-07-13T07:22:53Z

Why was such a basic and important feature rejected for a type system? That's a pity!

MartinJohns · 2023-07-13T10:39:19Z

@Autumn-one It wasn't rejected, the issue is still open: #4196

As to why it's not implemented yet? Priorities, time constraints, language constraints, limited resources. Feel free to fork the TypeScript repo and try to implement it, you'll see that it's not an easy task.

weswigham requested review from sandersn, DanielRosenwasser, rbuckton and ahejlsberg January 9, 2019 01:46

DanielRosenwasser reviewed Jan 9, 2019

View reviewed changes

weswigham closed this Jan 9, 2019

weswigham reopened this Jan 9, 2019

weswigham mentioned this pull request Jan 16, 2019

Exact Types #12936

Open

DanielRosenwasser reviewed Jan 23, 2019

View reviewed changes

RyanCavanaugh assigned weswigham Jan 24, 2019

jack-williams mentioned this pull request Jan 24, 2019

Provisional - Add not keyword emacs-typescript/typescript.el#98

Closed

whzx5byb mentioned this pull request Apr 7, 2022

Anonymous type parameters #48594

Open

jiangshanmeta mentioned this pull request May 10, 2022

TypeScript中为primitive type添加名义类型 jiangshanmeta/jiangshanmeta.github.io#45

Open

MartinJohns mentioned this pull request May 15, 2022

Typeguard not working if checked against Exclude #49118

Closed

bradzacher mentioned this pull request May 20, 2022

Enhancement: [@typescript-eslint/no-unnecessary-condition] Detect unnecessary comparison to falsy values typescript-eslint/typescript-eslint#5021

Closed

4 tasks

sandersn closed this May 24, 2022

fatcerberus mentioned this pull request Jun 11, 2022

Inconsistent property type inference #49463

Closed

sindresorhus mentioned this pull request Jul 7, 2022

Add Not<string, 'not me'> sindresorhus/type-fest#417

Open

jamiebuilds mentioned this pull request Jul 12, 2022

Template strings: Negated match #49867

Open

5 tasks

MartinJohns mentioned this pull request Oct 12, 2022

Support open-ended unions #26277

Open

4 tasks

MartinJohns mentioned this pull request Dec 19, 2022

Allow to remove keys from index type #51952

Closed

5 tasks

sacru2red mentioned this pull request Jan 3, 2023

allow constructing URLSearchParams directly from FormData #30584

Closed

gvergnaud mentioned this pull request Jan 22, 2023

.with and Pattern.not error since 4.1.3 gvergnaud/ts-pattern#138

Closed

MartinJohns mentioned this pull request Mar 30, 2023

Exclude is bottlenecked by depth limit #53583

Closed

gismya mentioned this pull request Apr 4, 2023

fix: bug in typings after recent PR ftrackhq/ftrack-javascript#95

Merged

4 tasks

0-CAT mentioned this pull request Jun 1, 2023

Add XMP raw string type to ExpandedTags["xmp"] type mattiasw/ExifReader#197

Merged

Autumn-one mentioned this pull request Jul 13, 2023

Supporting negative types is very convenient #55000

Closed

5 tasks

fatcerberus mentioned this pull request Aug 2, 2023

Partially discriminated union with explicitly defined key loosens inferred type #55239

Closed

kevinbarabash mentioned this pull request Dec 17, 2023

Negation types escalier-lang/escalier-next#75

Open

aaditmshah mentioned this pull request Feb 4, 2024

Intersection of conditional types, acting on a generic type, with another type doesn't narrow the generic type #57246

Closed

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Negated types #29317

Negated types #29317

weswigham commented Jan 9, 2019 •

edited

Loading

DanielRosenwasser Jan 9, 2019

weswigham Jan 9, 2019

DanielRosenwasser commented Jan 9, 2019

weswigham commented Jan 9, 2019 •

edited

Loading

DanielRosenwasser commented Jan 9, 2019 •

edited by weswigham

Loading

weswigham commented Jan 9, 2019 •

edited

Loading

weswigham commented Jan 9, 2019 •

edited

Loading

Jessidhia commented Jan 10, 2019

weswigham commented Jan 10, 2019

Jessidhia commented Jan 10, 2019

jack-williams commented Jan 10, 2019 •

edited

Loading

weswigham commented Jan 10, 2019 •

edited

Loading

jack-williams commented Jan 10, 2019

weswigham commented Jan 10, 2019 •

edited

Loading

SalathielGenese commented Jan 15, 2019 •

edited

Loading

jack-williams commented Jan 16, 2019

weswigham commented Jan 16, 2019

DanielRosenwasser Jan 23, 2019

peter-leonov Jan 23, 2019

jack-williams commented Jan 24, 2019 •

edited

Loading

weswigham commented Jan 24, 2019 •

edited

Loading

jack-williams commented Jan 24, 2019

qwelias commented May 15, 2022

kevinbarabash commented May 24, 2022

sandersn commented May 24, 2022

jsejcksn commented May 24, 2022

sandersn commented May 25, 2022

weswigham commented May 25, 2022 •

edited

Loading

dimitropoulos commented Jun 1, 2022

sandersn commented Jun 1, 2022

falfiya commented Jun 7, 2022

Autumn-one commented Jul 13, 2023

MartinJohns commented Jul 13, 2023

Negated types #29317

Negated types #29317

Conversation

weswigham commented Jan 9, 2019 • edited Loading

Negated Types

Syntax

Identities

Assignability Rules

Assignability Addendum for Fresh Object Types

Examples

DanielRosenwasser Jan 9, 2019

Choose a reason for hiding this comment

weswigham Jan 9, 2019

Choose a reason for hiding this comment

DanielRosenwasser commented Jan 9, 2019

weswigham commented Jan 9, 2019 • edited Loading

DanielRosenwasser commented Jan 9, 2019 • edited by weswigham Loading

weswigham commented Jan 9, 2019 • edited Loading

weswigham commented Jan 9, 2019 • edited Loading

Jessidhia commented Jan 10, 2019

weswigham commented Jan 10, 2019

Jessidhia commented Jan 10, 2019

jack-williams commented Jan 10, 2019 • edited Loading

weswigham commented Jan 10, 2019 • edited Loading

jack-williams commented Jan 10, 2019

weswigham commented Jan 10, 2019 • edited Loading

SalathielGenese commented Jan 15, 2019 • edited Loading

jack-williams commented Jan 16, 2019

weswigham commented Jan 16, 2019

DanielRosenwasser Jan 23, 2019

Choose a reason for hiding this comment

peter-leonov Jan 23, 2019

Choose a reason for hiding this comment

jack-williams commented Jan 24, 2019 • edited Loading

weswigham commented Jan 24, 2019 • edited Loading

jack-williams commented Jan 24, 2019

qwelias commented May 15, 2022

kevinbarabash commented May 24, 2022

sandersn commented May 24, 2022

jsejcksn commented May 24, 2022

sandersn commented May 25, 2022

weswigham commented May 25, 2022 • edited Loading

dimitropoulos commented Jun 1, 2022

sandersn commented Jun 1, 2022

falfiya commented Jun 7, 2022

Autumn-one commented Jul 13, 2023

MartinJohns commented Jul 13, 2023

weswigham commented Jan 9, 2019 •

edited

Loading

weswigham commented Jan 9, 2019 •

edited

Loading

DanielRosenwasser commented Jan 9, 2019 •

edited by weswigham

Loading

weswigham commented Jan 9, 2019 •

edited

Loading

weswigham commented Jan 9, 2019 •

edited

Loading

jack-williams commented Jan 10, 2019 •

edited

Loading

weswigham commented Jan 10, 2019 •

edited

Loading

weswigham commented Jan 10, 2019 •

edited

Loading

SalathielGenese commented Jan 15, 2019 •

edited

Loading

jack-williams commented Jan 24, 2019 •

edited

Loading

weswigham commented Jan 24, 2019 •

edited

Loading

weswigham commented May 25, 2022 •

edited

Loading